Single Binaries #1730
Merged
Single Binaries #1730
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
JasonGross
force-pushed
the
single-binary
branch
8 times, most recently
from
c4ca3e1 to
9f9c511
Compare
JasonGross
force-pushed
the
single-binary
branch
4 times, most recently
from
4964ba1 to
f0be03c
Compare
Fixes mit-plv#1724 Note that we keep the non-unified binaries (and use them to build generated files) to avoid OOMs on Coq's CI. It's unfortunate that compilation is so slow here, taking almost an hour on my machine just to extract and compile the various binaries. <details><summary>Timing Diff</summary> <p> ``` Time | Peak Mem | File Name ---------------------------------------------------------------------------------- 53m02.47s | 2463008 ko | Total Time / Peak Mem ---------------------------------------------------------------------------------- 2m21.70s | 2462928 ko | ExtractionOCaml/fiat_crypto 2m19.85s | 2463008 ko | ExtractionOCaml/bedrock2_fiat_crypto 1m53.82s | 1863716 ko | ExtractionOCaml/solinas_reduction 1m36.75s | 2462904 ko | ExtractionOCaml/with_bedrock2_fiat_crypto 1m33.30s | 2316820 ko | ExtractionOCaml/bedrock2_fiat_crypto.ml 1m30.98s | 2300660 ko | ExtractionOCaml/fiat_crypto.ml 1m30.25s | 2075840 ko | ExtractionOCaml/with_bedrock2_word_by_word_montgomery 1m26.51s | 2074640 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery 1m25.26s | 1829432 ko | ExtractionOCaml/word_by_word_montgomery 1m22.38s | 1780504 ko | ExtractionOCaml/bedrock2_unsaturated_solinas 1m20.72s | 2147524 ko | ExtractionOCaml/bedrock2_solinas_reduction 1m20.62s | 2336764 ko | ExtractionOCaml/with_bedrock2_fiat_crypto.ml 1m18.57s | 1416332 ko | ExtractionOCaml/with_bedrock2_base_conversion 1m16.74s | 1469000 ko | ExtractionOCaml/bedrock2_dettman_multiplication 1m14.80s | 1780196 ko | ExtractionOCaml/with_bedrock2_unsaturated_solinas 1m14.67s | 1415232 ko | ExtractionOCaml/base_conversion 1m08.91s | 1416276 ko | ExtractionOCaml/bedrock2_base_conversion 1m08.90s | 1415436 ko | ExtractionOCaml/dettman_multiplication 1m07.90s | 1415368 ko | ExtractionOCaml/saturated_solinas 1m07.63s | 1525784 ko | ExtractionOCaml/unsaturated_solinas 1m07.23s | 1449720 ko | ExtractionOCaml/with_bedrock2_dettman_multiplication 1m07.09s | 1447196 ko | ExtractionOCaml/with_bedrock2_saturated_solinas 1m07.02s | 1439752 ko | ExtractionOCaml/bedrock2_saturated_solinas 1m06.29s | 1448860 ko | ExtractionOCaml/with_bedrock2_solinas_reduction 1m05.35s | 2190452 ko | ExtractionOCaml/bedrock2_solinas_reduction.ml 1m03.87s | 2137192 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery.ml 1m01.18s | 2137308 ko | ExtractionOCaml/with_bedrock2_word_by_word_montgomery.ml 0m58.53s | 2057100 ko | ExtractionOCaml/solinas_reduction.ml 0m56.27s | 2063328 ko | ExtractionOCaml/with_bedrock2_unsaturated_solinas.ml 0m55.76s | 1836424 ko | ExtractionOCaml/perf_word_by_word_montgomery.ml 0m55.38s | 2030208 ko | ExtractionOCaml/word_by_word_montgomery.ml 0m52.90s | 1413320 ko | ExtractionOCaml/perf_unsaturated_solinas 0m51.44s | 2063536 ko | ExtractionOCaml/bedrock2_unsaturated_solinas.ml 0m51.16s | 1950720 ko | ExtractionOCaml/bedrock2_base_conversion.ml 0m50.96s | 1989736 ko | ExtractionOCaml/bedrock2_dettman_multiplication.ml 0m49.61s | 1936244 ko | ExtractionOCaml/with_bedrock2_solinas_reduction.ml 0m49.39s | 1936412 ko | ExtractionOCaml/with_bedrock2_saturated_solinas.ml 0m49.38s | 1753040 ko | ExtractionOCaml/perf_unsaturated_solinas.ml 0m48.72s | 1938204 ko | ExtractionOCaml/with_bedrock2_dettman_multiplication.ml 0m48.29s | 1952524 ko | ExtractionOCaml/with_bedrock2_base_conversion.ml 0m48.16s | 1938444 ko | ExtractionOCaml/bedrock2_saturated_solinas.ml 0m47.28s | 1962520 ko | ExtractionOCaml/unsaturated_solinas.ml 0m46.15s | 1823484 ko | ExtractionOCaml/base_conversion.ml 0m42.74s | 1413036 ko | ExtractionOCaml/perf_word_by_word_montgomery 0m41.95s | 1882704 ko | ExtractionOCaml/dettman_multiplication.ml 0m38.36s | 1846056 ko | ExtractionOCaml/saturated_solinas.ml 0m04.57s | 1035968 ko | Rewriter/PerfTesting/StandaloneOCamlMain.vo 0m00.93s | 106556 ko | ExtractionOCaml/bedrock2_unsaturated_solinas.cmi 0m00.90s | 102844 ko | ExtractionOCaml/bedrock2_fiat_crypto.cmi 0m00.89s | 103608 ko | ExtractionOCaml/dettman_multiplication.cmi 0m00.87s | 105352 ko | ExtractionOCaml/unsaturated_solinas.cmi 0m00.84s | 102728 ko | ExtractionOCaml/fiat_crypto.cmi 0m00.83s | 103608 ko | ExtractionOCaml/saturated_solinas.cmi 0m00.83s | 103844 ko | ExtractionOCaml/with_bedrock2_fiat_crypto.cmi 0m00.81s | 102720 ko | ExtractionOCaml/with_bedrock2_saturated_solinas.cmi 0m00.80s | 103684 ko | ExtractionOCaml/bedrock2_saturated_solinas.cmi 0m00.76s | 102640 ko | ExtractionOCaml/with_bedrock2_solinas_reduction.cmi 0m00.76s | 107620 ko | ExtractionOCaml/with_bedrock2_unsaturated_solinas.cmi 0m00.75s | 102300 ko | ExtractionOCaml/bedrock2_dettman_multiplication.cmi 0m00.75s | 103592 ko | ExtractionOCaml/with_bedrock2_base_conversion.cmi 0m00.75s | 102900 ko | ExtractionOCaml/with_bedrock2_word_by_word_montgomery.cmi 0m00.74s | 102780 ko | ExtractionOCaml/bedrock2_base_conversion.cmi 0m00.72s | 103088 ko | ExtractionOCaml/bedrock2_word_by_word_montgomery.cmi 0m00.71s | 105644 ko | ExtractionOCaml/word_by_word_montgomery.cmi 0m00.70s | 103272 ko | ExtractionOCaml/base_conversion.cmi 0m00.69s | 103100 ko | ExtractionOCaml/with_bedrock2_dettman_multiplication.cmi 0m00.67s | 102580 ko | ExtractionOCaml/bedrock2_solinas_reduction.cmi 0m00.67s | 103236 ko | ExtractionOCaml/solinas_reduction.cmi 0m00.42s | 58808 ko | ExtractionOCaml/perf_word_by_word_montgomery.cmi 0m00.39s | 60084 ko | ExtractionOCaml/perf_unsaturated_solinas.cmi ``` </p> </details>
JasonGross
force-pushed
the
single-binary
branch
from
f0be03c to
c8dd96c
Compare
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Very much a work in progress, not sure if I'll find time to finish this, creating this PR so it's not lost. (Very happy to have someone adopt this out from under me.)I expect there's maybe 1 more hour of work to do on this:firstn argv 2, passes(prog_name_count:=2)to the pipelines it delegates to,(Wakatime claims I've spent 38 mins 29 secs on this so far.)(Wakatime claims I've spent 2 hrs 10 mins on this branch)
Fixes #1724
cc @andres-erbsen, you were interested in this
Note that we keep the non-unified binaries (and use them to build
generated files) to avoid OOMs on Coq's CI.
It's unfortunate that compilation is so slow here, taking almost an hour
on my machine just to extract and compile the various binaries. (The unified binaries (one without bedrock2 and two with bedrock2) take about 10m19s to extract and compile.)
Timing Diff